<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Extraction: 从 Coq 中提取 ML</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Extraction<span class="subtitle">从 Coq 中提取 ML</span></h1>


<div class="doc">

<div class="paragraph"> </div>

<a name="lab390"></a><h1 class="section">基本的提取方式</h1>

<div class="paragraph"> </div>

 对于用 Coq 编写的代码而言，从中提取高效程序的最简方式是十分直白的。

<div class="paragraph"> </div>

    首先我们需要指定提取的目标语言。可选的语言有三种：提取机制最为成熟的
    OCaml，提取结果大都可以直接使用的 Haskell，以及提取机制有些过时的 Scheme。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="var">Coq.extraction.Extraction</span>.<br/>
<span class="id" type="var">Extraction</span> <span class="id" type="var">Language</span> <span class="id" type="var">OCaml</span>.<br/>
</div>

<div class="doc">
现在我们将待提取的定义加载到 Coq 环境中。你可以直接写出定义，
    也可以从其它模块中加载。 
</div>
<div class="code code-tight">

<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Init.Nat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.EqNat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ImpCEvalFun</span>.<br/>
</div>

<div class="doc">
最后，我们来指定需要提取的定义，以及用于保存提取结果的文件名。 
</div>
<div class="code code-tight">

<span class="id" type="var">Extraction</span> "imp1.ml" <span class="id" type="var">ceval_step</span>.<br/>
</div>

<div class="doc">
Coq 在处理此指令时会生成一个名为 <span class="inlinecode"><span class="id" type="var">imp1.ml</span></span> 的文件，其中包含了提取后的
    <span class="inlinecode"><span class="id" type="var">ceval_step</span></span> 以及所有递归依赖的文件。编译本章对应的 <span class="inlinecode">.<span class="id" type="var">v</span></span>
    文件，然后看看生成的 <span class="inlinecode"><span class="id" type="var">imp1.ml</span></span> 吧！ 
</div>

<div class="doc">
<a name="lab391"></a><h1 class="section">控制提取特定的类型</h1>

<div class="paragraph"> </div>

 我们可以让 Coq 将具体的 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 定义提取为特定的 OCaml 类型。
    对于每一个定义，我们都要指明：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 该 Coq 类型应当如何用 OCaml 来表示，以及

</li>
<li> 该类型的构造子应如何转换为目标语言中对应的标识符。 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">bool</span> ⇒ "bool" [ "true" "false" ].<br/>
</div>

<div class="doc">
对于非枚举类型（即构造器接受参数的类型），我们需要给出一个 OCaml
    表达式来作为该类型元素上的“递归器”。（想想丘奇数。）

<div class="paragraph"> </div>

    （译注：在这一部分，读者可以在为 <span class="inlinecode"><span class="id" type="var">nat</span></span> 指定对应的类型后使用
    <span class="inlinecode"><span class="id" type="var">Extraction</span></span> <span class="inlinecode"><span class="id" type="var">plus</span></span> 来得到自然数加法的提取结果，以此加深对“递归器”的理解。）
</div>
<div class="code code-tight">

<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">nat</span> ⇒ "int"<br/>
&nbsp;&nbsp;[ "0" "(fun x → x + 1)" ]<br/>
&nbsp;&nbsp;"(fun zero succ n →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if n=0 then zero () else succ (n-1))".<br/>
</div>

<div class="doc">
我们也可以将定义的常量提取为具体的 OCaml 项或者操作符。 
</div>
<div class="code code-tight">

<span class="id" type="var">Extract</span> <span class="id" type="var">Constant</span> <span class="id" type="var">plus</span> ⇒ "( + )".<br/>
<span class="id" type="var">Extract</span> <span class="id" type="var">Constant</span> <span class="id" type="var">mult</span> ⇒ "( * )".<br/>
<span class="id" type="var">Extract</span> <span class="id" type="var">Constant</span> <span class="id" type="var">eqb</span> ⇒ "( = )".<br/>
</div>

<div class="doc">
注意：保证提取结果的合理性是<b>你的责任</b>。例如，以下指定可能十分自然：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Extract</span>&nbsp;<span class="id" type="var">Constant</span>&nbsp;<span class="id" type="var">minus</span>&nbsp;⇒&nbsp;"( - )".
<div class="paragraph"> </div>

</div>
    但是这样做会引起严重的混乱。（思考一下。为什么会这样呢？）

</div>
<div class="code code-tight">

<span class="id" type="var">Extraction</span> "imp2.ml" <span class="id" type="var">ceval_step</span>.<br/>
</div>

<div class="doc">
检查一下生成的 <span class="inlinecode"><span class="id" type="var">imp2.ml</span></span> 文件，留意一下此次的提取结果与 <span class="inlinecode"><span class="id" type="var">imp1.ml</span></span>
    有何不同。 
</div>

<div class="doc">
<a name="lab392"></a><h1 class="section">一个完整的示例</h1>

<div class="paragraph"> </div>

 为了使用提取的求值器运行 Imp 程序，我们还需要一个小巧的驱动程序
    来调用求值器并输出求值结果。

<div class="paragraph"> </div>

    为简单起见，我们只取最终状态下前四个存储空间中的内容作为程序的结果。
    （译注：这里的存储空间指作为状态的 <span class="inlinecode"><span class="id" type="var">map</span></span>。）

<div class="paragraph"> </div>

    为了更方便地输入例子，我们将会从 <span class="inlinecode"><span class="id" type="var">ImpParser</span></span> 模块中提取出语法解析器。
    首先需要正确建立 Coq 中的字符串与 OCaml 中字符列表的对应关系。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ExtrOcamlBasic</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ExtrOcamlString</span>.<br/>
</div>

<div class="doc">
我们还需要翻译另一种布尔值： 
</div>
<div class="code code-tight">

<span class="id" type="var">Extract</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">sumbool</span> ⇒ "bool" ["true" "false"].<br/>
</div>

<div class="doc">
提取指令是相同的。 
</div>
<div class="code code-tight">

<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ImpParser</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">Extraction</span> "imp.ml" <span class="id" type="var">empty_st</span> <span class="id" type="var">ceval_step</span> <span class="id" type="var">parse</span>.<br/>
</div>

<div class="doc">
现在我们来运行一下生成的 Imp 求值器。首先你应该阅览一下
    <span class="inlinecode"><span class="id" type="var">impdriver.ml</span></span>（这并非从某个 Coq 源码提取而来，它是手写的。）

<div class="paragraph"> </div>

    然后用下面的指令将求值器与驱动程序一同编译成可执行文件：
<pre>
        ocamlc -w -20 -w -26 -o impdriver imp.mli imp.ml impdriver.ml
        ./impdriver
</pre>
    （编译时所使用的 <span class="inlinecode">-<span class="id" type="var">w</span></span> 开关只是为了避免输出一些误报的警告信息。） 
</div>

<div class="doc">
<a name="lab393"></a><h1 class="section">讨论</h1>

<div class="paragraph"> </div>

 由于我们证明了 <span class="inlinecode"><span class="id" type="var">ceval_step</span></span> 函数的行为在适当的意义上与 <span class="inlinecode"><span class="id" type="var">ceval</span></span>
    关系一致，因此提取出的程序可视作<b>已验证的</b> Imp 解释器。
    当然，我们使用的语法分析器并未经过验证，因为我们并未对它进行任何证明！ 
</div>

<div class="doc">
<a name="lab394"></a><h1 class="section">更进一步</h1>

<div class="paragraph"> </div>

 有关提取的更多详情见<b>软件基础</b>第三卷<b>已验证的函数式算法</b>中的
    Extract 一章。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:25&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>